COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	* 12. ∀U.SEXP U
C00004 00003	14 is an unknown mode operator.
C00007 ENDMK
C⊗;
* 12. ∀U.SEXP U
* 13. ∀X U.LISTP CONS(X,U)
* 14. ∀X U.LISTP X~U
* 15. ∀U.NULL U≡U=NNIL
* 16. ∀X U.¬NULL CONS(X,U)
* 17. ∀X U.¬NULL X~U
* 18. ∀X U.CAR CONS(X,U)=X
* 19. ∀X U.CAR (X~U)=X
* 20. ∀X U.CDR CONS(X,U)=U
* 21. ∀X U.CDR (X~U)=U
* 22. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
* 23. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
* 
* 25. ∀U V.LISTP U*V
* 26. ∀U V.U*V=IF NULL U THEN V ELSE CONS(CAR U,CDR U*V)
* 27. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
* 
* 
* 30. ∀X.LISTP LIST(X)
* 31. ∀X.LIST(X)=CONS(X,NNIL)
* 32. ∀X Y.LISTP LIST(X,Y)
* 33. ∀X Y.LIST(X,Y)=CONS(X,LIST(Y))
* 34. ∀X Y Z.LISTP LIST(X,Y,Z)
* 35. ∀X Y Z.LIST(X,Y,Z)=CONS(X,LIST(Y,Z))
* 36. ∀U.LISTP REVERSE U
* 37. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
* 38. ∀U.NNIL*U=U
* 39. ∀X U V.X~U*V=X~(U*V)
* 40. ∀U V W.(U*V)*W=U*(V*W)
* 41. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
14 is an unknown mode operator.
* 42. (∀V W.(NNIL*V)*W=NNIL*(V*W))∧
    (∀X U.(∀V W.(U*V)*W=U*(V*W))⊃(∀V W.(X~U*V)*W=X~U*(V*W)))⊃
     (∀U V W.(U*V)*W=U*(V*W))
    ctxt: (1 2 5 7 24)   deps: NIL

* 
(∀e phi |λu.∀v w.(u*v)*w = u*(v*w)| 23 nil (14 25))
43. (λU.∀V W.(U*V)*W=U*(V*W))(NNIL)∧
    (∀X U.(λU.∀V W.(U*V)*W=U*(V*W))(U)⊃(λU.∀V W.(U*V)*W=U*(V*W))(X~U))⊃
     (∀U.(λU.∀V W.(U*V)*W=U*(V*W))(U))
    ctxt: (1 2 5 7 24)   deps: NIL

* 
(∀e phi |λu.∀v w.(u*v)*w = u*(v*w)| 23 |*>38| (14 25))

44. (∀V W.V*W=V*W)∧(∀X U.(∀V W.(U*V)*W=U*(V*W))⊃(∀V W.(X~U*V)*W=X~U*(V*W)))⊃
     (∀U V W.(U*V)*W=U*(V*W))
    ctxt: (1 2 7 24)   deps: NIL

* 45. (∀X U.(∀V W.(U*V)*W=U*(V*W))⊃(∀V W.(X~U*V)*W=X~U*(V*W)))⊃
     (∀U V W.(U*V)*W=U*(V*W))
    ctxt: (1 2 7 24)   deps: NIL

* 
(rw 42 |*>38*nil| 25)

46. (NNIL*V)*W=NNIL*(V*W)∧(∀X U.(U*V)*W=U*(V*W)⊃(X~U*V)*W=X~U*(V*W))⊃
     (∀U.(U*V)*W=U*(V*W))
    ctxt: (1 2 5 7 24)   deps: NIL

47. (∀X U.(U*V)*W=U*(V*W)⊃(X~U*V)*W=X~U*(V*W))⊃(∀U.(U*V)*W=U*(V*W))
    ctxt: (1 2 7 24)   deps: NIL

* 
(rw 46 |*>38*nil| 25)

48. (∀X U.(U*V)*W=U*(V*W)⊃(X~U*V)*W=X~U*(V*W))⊃(∀U.(U*V)*W=U*(V*W))
    ctxt: (1 2 7 24)   deps: NIL

* 49. (∀X U.(U*V)*W=U*(V*W)⊃X~((U*V)*W)=X~(U*(V*W)))⊃(∀U.(U*V)*W=U*(V*W))
    ctxt: (1 2 7 24)   deps: NIL

*  failed to derive V*W=V*W∧(∀X U.(U*V)*W=U*(V*W)⊃X~((U*V)*W)=X~(U*(V*W)))⊃(∀U.(U*V)*W=U*(V*W))
cannot prove the following: 
(∀U.(∀X U.(U*V)*W=U*(V*W)⊃X~((U*V)*W)=X~(U*(V*W)))∧V*W=V*W∧LISTP U⊃
    (U*V)*W=U*(V*W))
* 
(rw 46 |*>38**>39*der*nil| 25)

* 
(∀e phi |λu.(u*v)*w = u*(v*w)| 23 nil (14 25))